\begin{tabbing}
$\forall$${\it the\_w}$:World.
\\[0ex]FairFifo
\\[0ex]$\Rightarrow$ \=($\forall$$e$:E.\+
\\[0ex]($\uparrow$isrcv(kind($e$)))
\\[0ex]$\Rightarrow$ (\=sends(lnk(kind($e$));sender($e$))[index($e$)]\+
\\[0ex]=
\\[0ex]msg(lnk(kind($e$));tag(kind($e$));val($e$))
\\[0ex]$\in$ Msg(${\it the\_w}$.M)))
\-\-
\end{tabbing}